Calculus of Constructions
-------------------------

<!--
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.

SPDX-License-Identifier: CC0-1.0
-->

[(Up)](../../README.md#topics) | _See also: [Coq](../Coq/README.md#coq)_

- - - -


### Web resources

[Calculus of constructions - Wikipedia](https://en.wikipedia.org/wiki/Calculus_of_constructions)

[lo.logic - Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic - Theoretical Computer Science Stack Exchange](https://cstheory.stackexchange.com/questions/53656/intuitive-explanation-of-the-fact-that-the-calculus-of-constructions-is-not-cons) ★


### Repositories

[atennapel/coc-os: "operating system" based on the calculus of constructions](https://github.com/atennapel/coc-os) ★ [💭](commentary/Chris%20Pressey.md#atennapel-coc-os-operating-system-based-on-the-calculus-of-constructions)


### Papers

[Introduction to the Calculus of Inductive Constructions](https://inria.hal.science/hal-01094195/document) ★ [💭](commentary/Chris%20Pressey.md#introduction-to-the-calculus-of-inductive-constructions)

[The Calculus of Inductive Constructions](https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf) ★ [💭](commentary/Chris%20Pressey.md#the-calculus-of-inductive-constructions)